PACKAGE BODY Exp IS

   PROCEDURE ExpBis (A: IN OUT Integer; B: IN OUT Integer; C: OUT Integer) IS
   BEGIN
      --#PRE: A = A_anf AND A >= 0 AND B = B_anf AND B >= 0
      C := 1;
      --#BOUND: B
      --#INV1: B >= 0 AND ((A**B)*C) = (A_anf**B_anf)
      WHILE B > 0 LOOP
         --#BOUND: B/2
         --#INV2: B > 0 AND ((A**B)*C) = (A_anf**B_anf)
         WHILE B mod 2 = 0 LOOP
            A := (A*A);
            B := (B/2);
         END LOOP;
         C := (C*A);
         B := (B-1);
      END LOOP;
      --#POST: C = (A_anf**B_anf)
   END ExpBis;

   PROCEDURE ExpLin (A: IN Integer; E: IN Integer; C: OUT Integer) IS
      B: Integer := E;
   BEGIN
      --#PRE: A = A_anf AND A >= 0 AND E = E_anf AND B = E AND B >= 0
      C := 1;
      --#BOUND: B
      --#INV: B >= 0 AND ((A**B)*C) = (A_anf**E_anf)
      WHILE(B > 0) LOOP
         C := C*A;
         B := B-1;
      END LOOP;
      --#POST: C = (A_anf**E_anf)
   END ExpLin;

END Exp;

